The Runtime Complexity (innermost) of the given CpxTRS could be proven to be BOUNDS(O(1), O(n^1)).

(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

0(x1) → 1(x1)
0(0(x1)) → 0(x1)
3(4(5(x1))) → 4(3(5(x1)))
2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → 0(1(1(1(1(1(0(1(1(0(0(1(1(0(1(1(1(0(1(0(1(1(0(1(0(1(1(1(1(0(1(1(0(1(1(0(0(1(1(0(1(0(1(0(0(1(1(1(0(0(1(1(0(0(0(1(0(1(0(1(0(0(0(0(0(0(1(0(0(0(0(0(1(0(1(0(0(1(0(0(0(1(1(0(1(0(1(0(1(1(0(1(0(1(1(1(1(0(1(1(1(0(0(1(0(0(1(0(1(1(1(0(1(0(1(1(1(0(0(0(0(1(1(1(1(1(0(1(1(1(0(1(1(0(0(0(0(0(1(0(1(1(1(1(0(0(1(1(1(1(0(0(0(1(0(1(1(0(1(1(1(1(1(1(0(1(0(1(1(0(0(0(0(1(1(0(1(1(0(0(0(0(1(0(0(0(1(1(1(1(1(0(0(0(0(0(0(1(1(0(1(0(0(1(1(0(1(1(0(0(1(0(1(0(1(0(1(1(0(0(0(1(1(1(0(1(1(0(1(1(0(0(0(0(0(1(1(0(1(1(0(0(0(0(1(1(0(0(1(1(0(1(0(1(0(1(1(1(1(1(1(0(0(1(0(0(1(1(0(0(0(0(0(0(0(0(0(0(0(1(1(1(1(0(1(0(0(1(0(0(1(1(0(1(0(0(0(1(0(1(0(1(1(1(1(0(0(0(0(1(1(0(1(0(0(1(0(1(0(0(0(0(1(1(1(1(1(0(0(1(1(0(1(0(0(0(1(0(0(0(0(0(1(0(1(0(0(0(1(1(0(0(0(0(1(1(1(1(0(1(x1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
1(1(0(1(0(0(0(0(1(1(1(0(1(1(1(1(0(0(0(0(0(0(1(1(1(1(1(0(1(0(1(0(1(0(1(0(0(1(1(1(1(1(0(1(0(0(1(1(1(1(0(0(0(0(1(0(1(1(1(0(0(0(1(0(0(0(1(0(0(0(0(1(0(1(1(1(1(1(0(1(1(1(0(0(1(0(1(1(0(1(1(0(1(0(0(1(1(0(1(1(1(1(1(1(1(0(1(0(0(1(1(1(0(0(0(0(1(0(1(0(0(1(1(1(1(0(0(0(1(0(0(0(0(0(0(1(0(1(1(1(1(1(0(0(1(0(0(0(0(0(0(0(1(0(0(1(1(1(0(1(0(0(1(1(0(0(1(0(1(1(0(1(1(0(1(0(1(0(0(1(0(0(1(1(0(1(1(1(1(0(0(0(1(1(0(0(1(0(0(0(1(0(0(1(0(1(1(0(0(1(0(0(0(1(0(1(1(1(0(0(0(1(1(0(0(0(1(0(1(0(1(1(0(0(0(1(0(1(1(0(1(0(1(0(0(1(0(1(1(0(1(0(0(1(0(1(0(1(1(0(1(1(0(1(0(0(0(0(1(0(0(1(0(0(1(1(1(0(0(0(1(0(0(0(0(0(1(1(1(0(1(0(0(1(1(1(1(1(1(0(0(1(1(1(0(0(1(0(1(0(0(0(0(1(0(1(1(0(0(1(0(1(1(0(0(1(1(0(0(0(1(0(1(1(1(1(0(0(0(0(0(1(1(0(1(1(1(1(1(1(1(0(0(0(1(1(0(1(0(1(1(1(0(1(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) → 2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(2(x1)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

Rewrite Strategy: INNERMOST

(1) CpxTrsMatchBoundsProof (EQUIVALENT transformation)

A linear upper bound on the runtime complexity of the TRS R could be shown with a Match Bound [MATCHBOUNDS1,MATCHBOUNDS2] of 1.
The certificate found is represented by the following graph.

Start state: 6
Accept states: [7, 8, 9, 10]
Transitions:
6→7[0_1|0, 1_1|1]
6→8[3_1|0]
6→9[2_1|0]
6→10[1_1|0]
6→6[4_1|0, 5_1|0]
6→11[5_1|1]
11→12[3_1|1]
12→8[4_1|1]

(2) BOUNDS(O(1), O(n^1))